Inference at * 2 1 1 1 
Iof proof for Lemma nth tl append:



1. T : Type
2. T List
3. T
4. v : T List
5. bs : T List
6. nth_tl(||v||;v @ bs) ~ bs
7. 0 < (||v||+1)
  ((||v||+1) - 1) ~ ||v|| 

latex

 by Auto' 

latex

 .

Definitions

n+m, #$n, nth_tl(n;as), as @ bs, ||as||, i  j , a < b, s ~ t, type List, Type, s = t, t  T, n - m